Nuprl Lemma : p-id_wf
11,40
postcript
pdf
T
:Type. p-id()
T
(
T
+ Top)
latex
ProofTree
Definitions
Type
,
t
T
,
Top
,
inl
x
,
x
.
A
(
x
)
,
x
:
A
.
B
(
x
)
,
p-id()
Lemmas
top
wf
origin
T:Type. p-id() 
T
(T + Top)
T:Type. p-id() T(T + Top)
T
x.A(x)x:A. B(x)